perm filename PRED.CMD[W77,JMC] blob
sn#259368 filedate 1977-01-25 generic text, type T, neo UTF8
ASSUME ∃n.(¬(n=zero)∧¬integer pred1(n,zero));
∃E ↑ n;
∧I induction;
∀E pred2 n,n1;
DISTRIB;
TAUT succ n1=n⊃pred1(n,n1)=n1 ↑↑:↑;
TAUT ¬(succ n1=n)⊃pred1(n,n1)=pred1(n,succ n1) ↑↑↑:↑↑;
ASSUME ¬integer pred1(n,n1);
∀E integer n1;
TAUTEQ ¬integer pred1(n,succ n1) 6:↑;
⊃I ↑↑↑⊃↑;
∀I ↑ n1;
TAUT ∀n1.¬integer pred1(n,n1) 2:3,↑;
∧I induction;
TAUTEQ succ n=succ n ;
∃I ↑ n←m OCC ((1));
TAUT (¬(n=zero)⊃∃m.succ m=n)⊃(¬(succ n=zero)⊃∃m.succ m=succ n) ↑;
∀I ↑ n;
TAUTEQ ∀n.(¬(n=zero)⊃∃m.succ m=n) 14,↑;
∀E pred2 succ m,m;
DISTRIB;
TAUT succ m=succ m⊃pred1(succ m,m)=m ↑↑:↑;
TAUTEQ pred1(succ m,m)=m ↑;
∀E integer m;
TAUTEQ integer pred1(succ m,m) ↑↑:↑;
∀I ↑ m;
∀E 19 n;
TAUT ∃m.succ m=n 2,↑;
∃E ↑ m;
SUBST ↑ IN 13;
∀E ↑ m;
TAUT FALSE 25,↑;
⊃I 1⊃↑;
TAUT ¬∃n.(¬(n=zero)∧¬integer pred1(n,zero)) ↑;
PUSH ↑;
∀E ↑ n;
∀E pred1 n;
TAUTEQ ¬(n=zero)⊃integer pred n ↑↑:↑;
∀I ↑ n;